T:Type, R:(TT), L:(T List), x, y:T. rel-path-between(T;R;x;y;L)   

latex

Definitions	Type, t  T, s = t, , x:AB(x), type List, b, False, P  Q, A, rel-path(R;L), a < b, f(a), x:A. B(x), x f y, ||as||, #$n, hd(l), , last(L), Void, <a, b>, A c B, P & Q, A  B, i  j , x:A  B(x), n+m, -n, n - m, i  j < k, , {x:A| B(x)} , {i..j}, l[i], rel-path-between(T;R;x;y;L), True
Lemmas	true wf, member wf, int seg wf, length wf1, select wf, hd wf, last wf, not wf, false wf, assert wf